This comment is confusing for me, aren't we adding this equation so we can work with the variable tmp inside the procedure? Like every other equation we create in handlers? This seems like the only reason is the lenghts.

Well, yes but. The main reason for the equalities is the length axiom adding. The mapping tmp -> replace_all(...) is stored separately as for the other string functions. In the final check we traverse all equalitions and recursively extract calls of replace_all and replacing them with the tmp variables. But these replacements are steered only by the function symbol mapping filled in handle_replace_all (and other such functions).

Yeah, it just seems weird to add such a comment here but not in other handlers (at least I feel there is something else in other handlers, am I wrong?). It seems from the comment like replace_all* have some special handling, which from the way I understood is true, but in a different way. But I do not fully understand what is happening with creating transducers, so maybe this comment makes sense here.